package ai.子句集;

import java.util.ArrayList;
import java.util.List;
import java.util.Stack;

public class ClauseSet {

    Sentence root = new Sentence();

    public ClauseSet() {

    }

    //∀ ∃ ∧ ∨ ～ >
    public void init() {
        String s = "∀x(∀y(P(x,y))>~∀y(Q(x,y)>R(x,y)))";

        //s = "~∃x(∀y(P(x,y)>Q(x,y)))";


        Stack<Sentence> stack = new Stack<>();

        Sentence now = root;

        for (int i = 0; i < s.length(); i++) {
            switch (s.charAt(i)) {
                case '~':
                    now.setRight(false);
                    break;
                case '∀':
                    now.setType(0);
                    //任意和存在后面必然是这个的内容
                    now.setString(String.valueOf(s.charAt(++i)));
                    break;
                case '∃':
                    now.setType(1);
                    //任意和存在后面必然是这个的内容
                    now.setString(String.valueOf(s.charAt(++i)));
                    break;
                case '(':
                    stack.push(now);
                    //遇到左括号就是孩子了
                    Sentence child = new Sentence();
                    child.setParent(now);
                    now.getChildSentenceList().add(child);
                    now = child;
                    break;
                case ')':
                    //这个pop出来的是兄弟节点
                    Sentence bother0 = stack.pop();
                    Sentence bother = new Sentence();
                    if (bother0.getParent() == null) break;
                    bother.setParent(bother0.getParent());
                    bother.getParent()
                            .getChildSentenceList()
                            .add(bother);
                    now = bother;
                    break;
                case '>':
                case '∧':
                case '∨':
                    int y = now.getParent().getChildSentenceList().size() - 1;
                    now.getParent().getRelationList().add(new Relation(y - 1, y, s.charAt(i)));
                    break;
                default:
                    now.setString(now.getString() + s.charAt(i));
            }
        }

        noChild(root);
    }
    
    //no child sentence remove...
    private void noChild(Sentence root) {
        if(root.getChildSentenceList().size() <= 0) {
            //remove empty sentence
            if(root.getString().length() > 0) {
                root.getParent().setString(root.getParent().getString() + '(' + root.getString() + ')');
            }
            root.getParent().getChildSentenceList().remove(root);
        } else {
            try{
                for(Sentence child : root.getChildSentenceList()) {
                    noChild(child);
                }
            }catch(Exception e) {}
            
        }
    }

    //消除蕴含和等值
    private void removeEqual(Sentence root) {
        //当前句子孩子间的所有关系
        for (int i = 0; i < root.getRelationList().size(); i++) {
            //如果是推出
            if (root.getRelationList().get(i).getRelation() == '>') {
                root.getChildSentenceList().get(root.getRelationList().get(i).getX()).setRight(false);
                root.getRelationList().get(i).setRelation('∨');
            }
        }

        //对它孩子进行递归移除
        for (Sentence child : root.getChildSentenceList()) {
            removeEqual(child);
        }
    }

    //缩小否定范围
    private void reduceScope(Sentence root) {
        //如果当前节点的是非状态时 非 的是否，才进行缩小否定范围
        if (!root.isRight()) {
            switch (root.getType()) {
                //任意
                case 0:
                    root.setType(1);
                    break;
                //存在
                case 1:
                    root.setType(0);
                    break;
                //普通句子
            }
            boolean isChanged = false;
            for (Relation relation : root.getRelationList()) {
                if (relation.getRelation() == '∧') {
                    root.setRight(true);

                    isChanged = true;
                    for (Sentence child : root.getChildSentenceList()) {
                        child.setRight(!child.isRight());
                    }
                    relation.setRelation('∨');
                }

                else if (relation.getRelation() == '∨') {
                    root.setRight(true);

                    isChanged = true;
                    for (Sentence child : root.getChildSentenceList()) {
                        child.setRight(!child.isRight());
                    }
                    relation.setRelation('∧');
                }
            }

            if (!isChanged) {
                for (Sentence child : root.getChildSentenceList()) {
                    root.setRight(true);

                    child.setRight(!child.isRight());
                }
            }
        }

        for (Sentence child : root.getChildSentenceList()) {
            reduceScope(child);
        }
    }

    //remove exist
    private void removeExist(Sentence root){
        //find exist
        if(root.getType() == 1) {
            //find it parent
            if(root.getParent() == null) {
                root.setType(-1);
                //set empty string to remove
                root.setString("");
            } else {
                //parent`s type is all
                if(root.getParent().getType() == 0) {
                    //set child
                    for(Sentence child : root.getChildSentenceList()) {
                        child.setString(child.getString().replace(root.getString(), "f(" + root.getParent().getString() + ")"));
                    }

                    root.setType(-1);
                    root.setString("");
                } else {
                    root.setType(-1);
                    root.setString("");
                }
            }
        }

        for(Sentence child : root.getChildSentenceList()) {
            removeExist(child);
        }
    }

    //remove all
    private void removeAll(Sentence root) {
        //if is all
        if(root.getType() == 0) {
            root.setType(-1);
            root.setString("");
        }

        for(Sentence child : root.getChildSentenceList()) {
            removeAll(child);
        }
    }

    //to hequ
    private void toHe(Sentence root) {
        //首先确保不是根节点
        if (root.getParent() != null) {
            //如果它有且只有一个兄弟，且他俩是或的关系
            if (root.getParent().getChildSentenceList().size() == 2 && root.getParent().getRelationList().get(0).getRelation() == '∨') {
                Sentence hasOneChild = null, hasTwoChild = null;
                for (Sentence rootChild : root.getParent().getChildSentenceList()) {
                    if (rootChild.getChildSentenceList().size() == 1) hasOneChild = rootChild;
                    else if (rootChild.getChildSentenceList().size() == 2) hasTwoChild = rootChild;
                }

                //到这里就可以判断需要化合取了
                if (hasTwoChild != null && hasTwoChild.getRelationList().get(0).getRelation() == '∧') {
                    Sentence twoChildFirst = hasTwoChild.getChildSentenceList().get(0);
                    Sentence newChild = new Sentence(
                            twoChildFirst.isRight(),
                            twoChildFirst.getType(),
                            twoChildFirst.getString(),
                            hasOneChild,
                            new ArrayList<>(),
                            new ArrayList<>());
                    hasOneChild.getChildSentenceList().add(newChild);

                    hasOneChild.getRelationList().add(new Relation(0, 1, '∨'));

                    hasTwoChild.getChildSentenceList().remove(0);

                    Sentence oneChildFirst = hasOneChild.getChildSentenceList().get(0);
                    Sentence newChild1 = new Sentence(
                            oneChildFirst.isRight(),
                            oneChildFirst.getType(),
                            oneChildFirst.getString(),
                            hasTwoChild,
                            new ArrayList<>(),
                            new ArrayList<>());
                    hasTwoChild.getChildSentenceList().add(0, newChild1);

                    hasTwoChild.getRelationList().get(0).setRelation('∨');

                    hasOneChild.getParent().getRelationList().get(0).setRelation('∧');
                }
            }
        }

        try {
            for(Sentence child : root.getChildSentenceList()) {
                toHe(child);
            }
        }catch (Exception e) {

        }
    }

    /**
     * 拆分成子句集
     * @param root
     */
    private String toSplit(Sentence root) {
        StringBuilder builder = new StringBuilder();
        builder.append('{');
        if (root.getRelationList().size() >= 1) {
            for (Relation relation : root.getRelationList()) {
                builder.append(root.getChildSentenceList().get(relation.getX()).show());
                if (relation.getRelation() == '∧') {
                    builder.append(',');
                } else {
                    builder.append(relation.getRelation());
                }
                builder.append(root.getChildSentenceList().get(relation.getY()).show());
            }
        } else {
            builder.append(root.getChildSentenceList().get(0).show());
        }
        builder.append('}');
        return builder.toString();
    }

    public static void main(String[] args) {
        ClauseSet clauseSet = new ClauseSet();
        clauseSet.init();
        clauseSet.removeEqual(clauseSet.root);
        clauseSet.reduceScope(clauseSet.root);
        clauseSet.removeExist(clauseSet.root);
        clauseSet.removeAll(clauseSet.root);
        clauseSet.toHe(clauseSet.root);

        System.out.println(clauseSet.toSplit(clauseSet.root));
    }
}

/**
 * 句子类
 */
class Sentence {
    //是否是 非句子，默认就是 是
    private boolean right;

    //全称、存在表示，-1表示既不是全称也不是存在，0是全称，1是存在
    private int type;

    //内容
    private String string;

    //这个句子的父节点
    private Sentence parent;

    private List<Sentence> childSentenceList;

    private List<Relation> relationList;

    public Sentence() {
        this.right = true;
        this.type = -1;
        this.string = "";
        this.parent = null;
        this.childSentenceList = new ArrayList<>();
        this.relationList = new ArrayList<>();
    }

    public Sentence(boolean right, int type, String string, Sentence parent, List<Sentence> childSentenceList, List<Relation> relationList) {
        this.right = right;
        this.type = type;
        this.string = string;
        this.parent = parent;
        this.childSentenceList = childSentenceList;
        this.relationList = relationList;
    }

    public boolean isRight() {
        return right;
    }

    public void setRight(boolean right) {
        this.right = right;
    }

    public int getType() {
        return type;
    }

    public void setType(int type) {
        this.type = type;
    }

    public String getString() {
        return string;
    }

    public void setString(String string) {
        this.string = string;
    }

    public Sentence getParent() {
        return parent;
    }

    public void setParent(Sentence parent) {
        this.parent = parent;
    }

    public List<Sentence> getChildSentenceList() {
        return childSentenceList;
    }

    public List<Relation> getRelationList() {
        return relationList;
    }

    public String show() {
        StringBuilder builder = new StringBuilder();
        if(!this.isRight()) builder.append("~");
        if(this.getType() == 0) builder.append("∀");
        else if(this.getType() == 1) builder.append("∃");
        builder.append(this.getString());
        builder.append("(");
        if (this.getRelationList().size() <= 0) {
            if (this.getChildSentenceList().size() >= 1) {
                builder.append(this.getChildSentenceList().get(0).show());
            }
        } else {
            for(Relation relation : this.getRelationList()) {
                builder.append(this.getChildSentenceList().get(relation.getX()).show());
                builder.append(relation.getRelation());
                builder.append(this.getChildSentenceList().get(relation.getY()).show());
            }
        }
        builder.append(")");
        return builder.toString().replace("()", "");
    }

    @Override
    public String toString() {
        return "\nSentence{" +
                "right=" + right +
                ", type=" + type +
                ", string='" + string + '\'' +
                ", childSentenceList=" + childSentenceList +
                ", relationList=" + relationList +
                "}\n";
    }
}

//关系类，用于存储兄弟之间的关系
class Relation {
    private int x;

    private int y;

    private char relation;

    public Relation(int x, int y, char relation) {
        this.x = x;
        this.y = y;
        this.relation = relation;
    }

    public int getX() {
        return x;
    }

    public void setX(int x) {
        this.x = x;
    }

    public int getY() {
        return y;
    }

    public void setY(int y) {
        this.y = y;
    }

    public char getRelation() {
        return relation;
    }

    public void setRelation(char relation) {
        this.relation = relation;
    }

    @Override
    public String toString() {
        return "Relation{" +
                "x=" + x +
                ", y=" + y +
                ", relation='" + relation + '\'' +
                '}';
    }
}


